ES(the_w)
== <E
== ,product-deq(Id;;IdDeq;NatDeq)
== ,(e.w-pred(the_w;e))
== ,(e.w-info(the_w;e))
== ,(TERMOF{w-order-axioms:ObjectId, 1:l, i:l}(the_w,p))
== ,the_w.T
== ,the_w.TA
== ,the_w.M
== ,(i,x. s(i;0).x)
== ,(i.1of(2of(w-machine(the_w;i))))
== ,(e.val(e))
== ,(i.2of(2of(w-machine(the_w;i))))
== ,(i.1of(w-machine(the_w;i)))
== ,(TERMOF{world-es-val:ObjectId, 1:l, i:l}(the_w,p))
== ,(TERMOF{world-es-atom:ObjectId, 1:l, i:l}(the_w,p))
== ,> 

latex

---

clarification:

w-es{i:l}
w-es(the_w; p)
== <w-E(the_w)
== ,product-deq(Id;;IdDeq;NatDeq)
== ,(e.w-pred(the_w;e))
== ,(e.w-info(the_w;e))
== ,(TERMOF{w-order-axioms:ObjectId, 1:l, i:l}(the_w,p))
== ,the_w.T
== ,the_w.TA
== ,the_w.M
== ,(i,x. w-s(the_w; i; 0; x))
== ,(i.1of(2of(w-machine(the_w;i))))
== ,(e.w-eval(the_w; e))
== ,(i.2of(2of(w-machine(the_w;i))))
== ,(i.1of(w-machine(the_w;i)))
== ,(TERMOF{world-es-val:ObjectId, 1:l, i:l}(the_w,p))
== ,(TERMOF{world-es-atom:ObjectId, 1:l, i:l}(the_w,p))
== ,> 

latex

Definitions	E, product-deq(A;B;a;b), Id, , IdDeq, NatDeq, w-pred(w;e), w-info(w;e), w-order-axioms, w.T, w.TA, w.M, s(i;t).x, #$n, val(e), 2of(t), x.A(x), 1of(t), w-machine(w;i), world-es-val, <a,b>, f(a), world-es-atom,
FDL editor aliases	w-es